Left Termination of the query pattern perm1_in_2(g, g) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

perm1(L, M) :- ','(eq_len1(L, M), same_sets(L, M)).
eq_len1([], []).
eq_len1(.(X, Xs), .(X1, Ys)) :- eq_len1(Xs, Ys).
member(X, .(X, X1)).
member(X, .(X1, T)) :- member(X, T).
same_sets([], X).
same_sets(.(X, Xs), L) :- ','(member(X, L), same_sets(Xs, L)).

Queries:

perm1(g,g).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

perm1_in(L, M) → U1(L, M, eq_len1_in(L, M))
eq_len1_in(.(X, Xs), .(X1, Ys)) → U3(X, Xs, X1, Ys, eq_len1_in(Xs, Ys))
eq_len1_in([], []) → eq_len1_out([], [])
U3(X, Xs, X1, Ys, eq_len1_out(Xs, Ys)) → eq_len1_out(.(X, Xs), .(X1, Ys))
U1(L, M, eq_len1_out(L, M)) → U2(L, M, same_sets_in(L, M))
same_sets_in(.(X, Xs), L) → U5(X, Xs, L, member_in(X, L))
member_in(X, .(X1, T)) → U4(X, X1, T, member_in(X, T))
member_in(X, .(X, X1)) → member_out(X, .(X, X1))
U4(X, X1, T, member_out(X, T)) → member_out(X, .(X1, T))
U5(X, Xs, L, member_out(X, L)) → U6(X, Xs, L, same_sets_in(Xs, L))
same_sets_in([], X) → same_sets_out([], X)
U6(X, Xs, L, same_sets_out(Xs, L)) → same_sets_out(.(X, Xs), L)
U2(L, M, same_sets_out(L, M)) → perm1_out(L, M)

The argument filtering Pi contains the following mapping:
perm1_in(x1, x2)  =  perm1_in(x1, x2)
U1(x1, x2, x3)  =  U1(x1, x2, x3)
eq_len1_in(x1, x2)  =  eq_len1_in(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4, x5)  =  U3(x5)
[]  =  []
eq_len1_out(x1, x2)  =  eq_len1_out
U2(x1, x2, x3)  =  U2(x3)
same_sets_in(x1, x2)  =  same_sets_in(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x3, x4)
member_in(x1, x2)  =  member_in(x1, x2)
U4(x1, x2, x3, x4)  =  U4(x4)
member_out(x1, x2)  =  member_out
U6(x1, x2, x3, x4)  =  U6(x4)
same_sets_out(x1, x2)  =  same_sets_out
perm1_out(x1, x2)  =  perm1_out

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

perm1_in(L, M) → U1(L, M, eq_len1_in(L, M))
eq_len1_in(.(X, Xs), .(X1, Ys)) → U3(X, Xs, X1, Ys, eq_len1_in(Xs, Ys))
eq_len1_in([], []) → eq_len1_out([], [])
U3(X, Xs, X1, Ys, eq_len1_out(Xs, Ys)) → eq_len1_out(.(X, Xs), .(X1, Ys))
U1(L, M, eq_len1_out(L, M)) → U2(L, M, same_sets_in(L, M))
same_sets_in(.(X, Xs), L) → U5(X, Xs, L, member_in(X, L))
member_in(X, .(X1, T)) → U4(X, X1, T, member_in(X, T))
member_in(X, .(X, X1)) → member_out(X, .(X, X1))
U4(X, X1, T, member_out(X, T)) → member_out(X, .(X1, T))
U5(X, Xs, L, member_out(X, L)) → U6(X, Xs, L, same_sets_in(Xs, L))
same_sets_in([], X) → same_sets_out([], X)
U6(X, Xs, L, same_sets_out(Xs, L)) → same_sets_out(.(X, Xs), L)
U2(L, M, same_sets_out(L, M)) → perm1_out(L, M)

The argument filtering Pi contains the following mapping:
perm1_in(x1, x2)  =  perm1_in(x1, x2)
U1(x1, x2, x3)  =  U1(x1, x2, x3)
eq_len1_in(x1, x2)  =  eq_len1_in(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4, x5)  =  U3(x5)
[]  =  []
eq_len1_out(x1, x2)  =  eq_len1_out
U2(x1, x2, x3)  =  U2(x3)
same_sets_in(x1, x2)  =  same_sets_in(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x3, x4)
member_in(x1, x2)  =  member_in(x1, x2)
U4(x1, x2, x3, x4)  =  U4(x4)
member_out(x1, x2)  =  member_out
U6(x1, x2, x3, x4)  =  U6(x4)
same_sets_out(x1, x2)  =  same_sets_out
perm1_out(x1, x2)  =  perm1_out


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

PERM1_IN(L, M) → U11(L, M, eq_len1_in(L, M))
PERM1_IN(L, M) → EQ_LEN1_IN(L, M)
EQ_LEN1_IN(.(X, Xs), .(X1, Ys)) → U31(X, Xs, X1, Ys, eq_len1_in(Xs, Ys))
EQ_LEN1_IN(.(X, Xs), .(X1, Ys)) → EQ_LEN1_IN(Xs, Ys)
U11(L, M, eq_len1_out(L, M)) → U21(L, M, same_sets_in(L, M))
U11(L, M, eq_len1_out(L, M)) → SAME_SETS_IN(L, M)
SAME_SETS_IN(.(X, Xs), L) → U51(X, Xs, L, member_in(X, L))
SAME_SETS_IN(.(X, Xs), L) → MEMBER_IN(X, L)
MEMBER_IN(X, .(X1, T)) → U41(X, X1, T, member_in(X, T))
MEMBER_IN(X, .(X1, T)) → MEMBER_IN(X, T)
U51(X, Xs, L, member_out(X, L)) → U61(X, Xs, L, same_sets_in(Xs, L))
U51(X, Xs, L, member_out(X, L)) → SAME_SETS_IN(Xs, L)

The TRS R consists of the following rules:

perm1_in(L, M) → U1(L, M, eq_len1_in(L, M))
eq_len1_in(.(X, Xs), .(X1, Ys)) → U3(X, Xs, X1, Ys, eq_len1_in(Xs, Ys))
eq_len1_in([], []) → eq_len1_out([], [])
U3(X, Xs, X1, Ys, eq_len1_out(Xs, Ys)) → eq_len1_out(.(X, Xs), .(X1, Ys))
U1(L, M, eq_len1_out(L, M)) → U2(L, M, same_sets_in(L, M))
same_sets_in(.(X, Xs), L) → U5(X, Xs, L, member_in(X, L))
member_in(X, .(X1, T)) → U4(X, X1, T, member_in(X, T))
member_in(X, .(X, X1)) → member_out(X, .(X, X1))
U4(X, X1, T, member_out(X, T)) → member_out(X, .(X1, T))
U5(X, Xs, L, member_out(X, L)) → U6(X, Xs, L, same_sets_in(Xs, L))
same_sets_in([], X) → same_sets_out([], X)
U6(X, Xs, L, same_sets_out(Xs, L)) → same_sets_out(.(X, Xs), L)
U2(L, M, same_sets_out(L, M)) → perm1_out(L, M)

The argument filtering Pi contains the following mapping:
perm1_in(x1, x2)  =  perm1_in(x1, x2)
U1(x1, x2, x3)  =  U1(x1, x2, x3)
eq_len1_in(x1, x2)  =  eq_len1_in(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4, x5)  =  U3(x5)
[]  =  []
eq_len1_out(x1, x2)  =  eq_len1_out
U2(x1, x2, x3)  =  U2(x3)
same_sets_in(x1, x2)  =  same_sets_in(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x3, x4)
member_in(x1, x2)  =  member_in(x1, x2)
U4(x1, x2, x3, x4)  =  U4(x4)
member_out(x1, x2)  =  member_out
U6(x1, x2, x3, x4)  =  U6(x4)
same_sets_out(x1, x2)  =  same_sets_out
perm1_out(x1, x2)  =  perm1_out
SAME_SETS_IN(x1, x2)  =  SAME_SETS_IN(x1, x2)
U51(x1, x2, x3, x4)  =  U51(x2, x3, x4)
EQ_LEN1_IN(x1, x2)  =  EQ_LEN1_IN(x1, x2)
U41(x1, x2, x3, x4)  =  U41(x4)
U31(x1, x2, x3, x4, x5)  =  U31(x5)
MEMBER_IN(x1, x2)  =  MEMBER_IN(x1, x2)
PERM1_IN(x1, x2)  =  PERM1_IN(x1, x2)
U61(x1, x2, x3, x4)  =  U61(x4)
U21(x1, x2, x3)  =  U21(x3)
U11(x1, x2, x3)  =  U11(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

PERM1_IN(L, M) → U11(L, M, eq_len1_in(L, M))
PERM1_IN(L, M) → EQ_LEN1_IN(L, M)
EQ_LEN1_IN(.(X, Xs), .(X1, Ys)) → U31(X, Xs, X1, Ys, eq_len1_in(Xs, Ys))
EQ_LEN1_IN(.(X, Xs), .(X1, Ys)) → EQ_LEN1_IN(Xs, Ys)
U11(L, M, eq_len1_out(L, M)) → U21(L, M, same_sets_in(L, M))
U11(L, M, eq_len1_out(L, M)) → SAME_SETS_IN(L, M)
SAME_SETS_IN(.(X, Xs), L) → U51(X, Xs, L, member_in(X, L))
SAME_SETS_IN(.(X, Xs), L) → MEMBER_IN(X, L)
MEMBER_IN(X, .(X1, T)) → U41(X, X1, T, member_in(X, T))
MEMBER_IN(X, .(X1, T)) → MEMBER_IN(X, T)
U51(X, Xs, L, member_out(X, L)) → U61(X, Xs, L, same_sets_in(Xs, L))
U51(X, Xs, L, member_out(X, L)) → SAME_SETS_IN(Xs, L)

The TRS R consists of the following rules:

perm1_in(L, M) → U1(L, M, eq_len1_in(L, M))
eq_len1_in(.(X, Xs), .(X1, Ys)) → U3(X, Xs, X1, Ys, eq_len1_in(Xs, Ys))
eq_len1_in([], []) → eq_len1_out([], [])
U3(X, Xs, X1, Ys, eq_len1_out(Xs, Ys)) → eq_len1_out(.(X, Xs), .(X1, Ys))
U1(L, M, eq_len1_out(L, M)) → U2(L, M, same_sets_in(L, M))
same_sets_in(.(X, Xs), L) → U5(X, Xs, L, member_in(X, L))
member_in(X, .(X1, T)) → U4(X, X1, T, member_in(X, T))
member_in(X, .(X, X1)) → member_out(X, .(X, X1))
U4(X, X1, T, member_out(X, T)) → member_out(X, .(X1, T))
U5(X, Xs, L, member_out(X, L)) → U6(X, Xs, L, same_sets_in(Xs, L))
same_sets_in([], X) → same_sets_out([], X)
U6(X, Xs, L, same_sets_out(Xs, L)) → same_sets_out(.(X, Xs), L)
U2(L, M, same_sets_out(L, M)) → perm1_out(L, M)

The argument filtering Pi contains the following mapping:
perm1_in(x1, x2)  =  perm1_in(x1, x2)
U1(x1, x2, x3)  =  U1(x1, x2, x3)
eq_len1_in(x1, x2)  =  eq_len1_in(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4, x5)  =  U3(x5)
[]  =  []
eq_len1_out(x1, x2)  =  eq_len1_out
U2(x1, x2, x3)  =  U2(x3)
same_sets_in(x1, x2)  =  same_sets_in(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x3, x4)
member_in(x1, x2)  =  member_in(x1, x2)
U4(x1, x2, x3, x4)  =  U4(x4)
member_out(x1, x2)  =  member_out
U6(x1, x2, x3, x4)  =  U6(x4)
same_sets_out(x1, x2)  =  same_sets_out
perm1_out(x1, x2)  =  perm1_out
SAME_SETS_IN(x1, x2)  =  SAME_SETS_IN(x1, x2)
U51(x1, x2, x3, x4)  =  U51(x2, x3, x4)
EQ_LEN1_IN(x1, x2)  =  EQ_LEN1_IN(x1, x2)
U41(x1, x2, x3, x4)  =  U41(x4)
U31(x1, x2, x3, x4, x5)  =  U31(x5)
MEMBER_IN(x1, x2)  =  MEMBER_IN(x1, x2)
PERM1_IN(x1, x2)  =  PERM1_IN(x1, x2)
U61(x1, x2, x3, x4)  =  U61(x4)
U21(x1, x2, x3)  =  U21(x3)
U11(x1, x2, x3)  =  U11(x1, x2, x3)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 3 SCCs with 8 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN(X, .(X1, T)) → MEMBER_IN(X, T)

The TRS R consists of the following rules:

perm1_in(L, M) → U1(L, M, eq_len1_in(L, M))
eq_len1_in(.(X, Xs), .(X1, Ys)) → U3(X, Xs, X1, Ys, eq_len1_in(Xs, Ys))
eq_len1_in([], []) → eq_len1_out([], [])
U3(X, Xs, X1, Ys, eq_len1_out(Xs, Ys)) → eq_len1_out(.(X, Xs), .(X1, Ys))
U1(L, M, eq_len1_out(L, M)) → U2(L, M, same_sets_in(L, M))
same_sets_in(.(X, Xs), L) → U5(X, Xs, L, member_in(X, L))
member_in(X, .(X1, T)) → U4(X, X1, T, member_in(X, T))
member_in(X, .(X, X1)) → member_out(X, .(X, X1))
U4(X, X1, T, member_out(X, T)) → member_out(X, .(X1, T))
U5(X, Xs, L, member_out(X, L)) → U6(X, Xs, L, same_sets_in(Xs, L))
same_sets_in([], X) → same_sets_out([], X)
U6(X, Xs, L, same_sets_out(Xs, L)) → same_sets_out(.(X, Xs), L)
U2(L, M, same_sets_out(L, M)) → perm1_out(L, M)

The argument filtering Pi contains the following mapping:
perm1_in(x1, x2)  =  perm1_in(x1, x2)
U1(x1, x2, x3)  =  U1(x1, x2, x3)
eq_len1_in(x1, x2)  =  eq_len1_in(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4, x5)  =  U3(x5)
[]  =  []
eq_len1_out(x1, x2)  =  eq_len1_out
U2(x1, x2, x3)  =  U2(x3)
same_sets_in(x1, x2)  =  same_sets_in(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x3, x4)
member_in(x1, x2)  =  member_in(x1, x2)
U4(x1, x2, x3, x4)  =  U4(x4)
member_out(x1, x2)  =  member_out
U6(x1, x2, x3, x4)  =  U6(x4)
same_sets_out(x1, x2)  =  same_sets_out
perm1_out(x1, x2)  =  perm1_out
MEMBER_IN(x1, x2)  =  MEMBER_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN(X, .(X1, T)) → MEMBER_IN(X, T)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MEMBER_IN(X, .(X1, T)) → MEMBER_IN(X, T)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U51(X, Xs, L, member_out(X, L)) → SAME_SETS_IN(Xs, L)
SAME_SETS_IN(.(X, Xs), L) → U51(X, Xs, L, member_in(X, L))

The TRS R consists of the following rules:

perm1_in(L, M) → U1(L, M, eq_len1_in(L, M))
eq_len1_in(.(X, Xs), .(X1, Ys)) → U3(X, Xs, X1, Ys, eq_len1_in(Xs, Ys))
eq_len1_in([], []) → eq_len1_out([], [])
U3(X, Xs, X1, Ys, eq_len1_out(Xs, Ys)) → eq_len1_out(.(X, Xs), .(X1, Ys))
U1(L, M, eq_len1_out(L, M)) → U2(L, M, same_sets_in(L, M))
same_sets_in(.(X, Xs), L) → U5(X, Xs, L, member_in(X, L))
member_in(X, .(X1, T)) → U4(X, X1, T, member_in(X, T))
member_in(X, .(X, X1)) → member_out(X, .(X, X1))
U4(X, X1, T, member_out(X, T)) → member_out(X, .(X1, T))
U5(X, Xs, L, member_out(X, L)) → U6(X, Xs, L, same_sets_in(Xs, L))
same_sets_in([], X) → same_sets_out([], X)
U6(X, Xs, L, same_sets_out(Xs, L)) → same_sets_out(.(X, Xs), L)
U2(L, M, same_sets_out(L, M)) → perm1_out(L, M)

The argument filtering Pi contains the following mapping:
perm1_in(x1, x2)  =  perm1_in(x1, x2)
U1(x1, x2, x3)  =  U1(x1, x2, x3)
eq_len1_in(x1, x2)  =  eq_len1_in(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4, x5)  =  U3(x5)
[]  =  []
eq_len1_out(x1, x2)  =  eq_len1_out
U2(x1, x2, x3)  =  U2(x3)
same_sets_in(x1, x2)  =  same_sets_in(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x3, x4)
member_in(x1, x2)  =  member_in(x1, x2)
U4(x1, x2, x3, x4)  =  U4(x4)
member_out(x1, x2)  =  member_out
U6(x1, x2, x3, x4)  =  U6(x4)
same_sets_out(x1, x2)  =  same_sets_out
perm1_out(x1, x2)  =  perm1_out
SAME_SETS_IN(x1, x2)  =  SAME_SETS_IN(x1, x2)
U51(x1, x2, x3, x4)  =  U51(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U51(X, Xs, L, member_out(X, L)) → SAME_SETS_IN(Xs, L)
SAME_SETS_IN(.(X, Xs), L) → U51(X, Xs, L, member_in(X, L))

The TRS R consists of the following rules:

member_in(X, .(X1, T)) → U4(X, X1, T, member_in(X, T))
member_in(X, .(X, X1)) → member_out(X, .(X, X1))
U4(X, X1, T, member_out(X, T)) → member_out(X, .(X1, T))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
member_in(x1, x2)  =  member_in(x1, x2)
U4(x1, x2, x3, x4)  =  U4(x4)
member_out(x1, x2)  =  member_out
SAME_SETS_IN(x1, x2)  =  SAME_SETS_IN(x1, x2)
U51(x1, x2, x3, x4)  =  U51(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

SAME_SETS_IN(.(X, Xs), L) → U51(Xs, L, member_in(X, L))
U51(Xs, L, member_out) → SAME_SETS_IN(Xs, L)

The TRS R consists of the following rules:

member_in(X, .(X1, T)) → U4(member_in(X, T))
member_in(X, .(X, X1)) → member_out
U4(member_out) → member_out

The set Q consists of the following terms:

member_in(x0, x1)
U4(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

EQ_LEN1_IN(.(X, Xs), .(X1, Ys)) → EQ_LEN1_IN(Xs, Ys)

The TRS R consists of the following rules:

perm1_in(L, M) → U1(L, M, eq_len1_in(L, M))
eq_len1_in(.(X, Xs), .(X1, Ys)) → U3(X, Xs, X1, Ys, eq_len1_in(Xs, Ys))
eq_len1_in([], []) → eq_len1_out([], [])
U3(X, Xs, X1, Ys, eq_len1_out(Xs, Ys)) → eq_len1_out(.(X, Xs), .(X1, Ys))
U1(L, M, eq_len1_out(L, M)) → U2(L, M, same_sets_in(L, M))
same_sets_in(.(X, Xs), L) → U5(X, Xs, L, member_in(X, L))
member_in(X, .(X1, T)) → U4(X, X1, T, member_in(X, T))
member_in(X, .(X, X1)) → member_out(X, .(X, X1))
U4(X, X1, T, member_out(X, T)) → member_out(X, .(X1, T))
U5(X, Xs, L, member_out(X, L)) → U6(X, Xs, L, same_sets_in(Xs, L))
same_sets_in([], X) → same_sets_out([], X)
U6(X, Xs, L, same_sets_out(Xs, L)) → same_sets_out(.(X, Xs), L)
U2(L, M, same_sets_out(L, M)) → perm1_out(L, M)

The argument filtering Pi contains the following mapping:
perm1_in(x1, x2)  =  perm1_in(x1, x2)
U1(x1, x2, x3)  =  U1(x1, x2, x3)
eq_len1_in(x1, x2)  =  eq_len1_in(x1, x2)
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4, x5)  =  U3(x5)
[]  =  []
eq_len1_out(x1, x2)  =  eq_len1_out
U2(x1, x2, x3)  =  U2(x3)
same_sets_in(x1, x2)  =  same_sets_in(x1, x2)
U5(x1, x2, x3, x4)  =  U5(x2, x3, x4)
member_in(x1, x2)  =  member_in(x1, x2)
U4(x1, x2, x3, x4)  =  U4(x4)
member_out(x1, x2)  =  member_out
U6(x1, x2, x3, x4)  =  U6(x4)
same_sets_out(x1, x2)  =  same_sets_out
perm1_out(x1, x2)  =  perm1_out
EQ_LEN1_IN(x1, x2)  =  EQ_LEN1_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

EQ_LEN1_IN(.(X, Xs), .(X1, Ys)) → EQ_LEN1_IN(Xs, Ys)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

EQ_LEN1_IN(.(X, Xs), .(X1, Ys)) → EQ_LEN1_IN(Xs, Ys)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: